(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(declare-fun v12 () Bool)
(declare-fun v15 () Bool)
(declare-fun r0 () Real)
(declare-fun r4 () Real)
(declare-fun r5 () Real)
(declare-fun arr-7381377837733731330_5932157297817509493-0 () (Array Real Bool))
(declare-fun v26 () Bool)
(declare-fun v28 () Bool)
(declare-fun arr-7381377837733731330_5932157297817509493-2 () (Array Real Bool))
(declare-fun v54 () Bool)
(check-sat)
